#ifndef ART_H
#define ART_H
#include "cfa.h"
#include <iostream>
#include <map>
#include "smt.h"
using namespace std;

struct ArtNode{
    Node* cfa_node;           //對應的cfa node
    vector<Prop*> predicate;  //可以用的predicate
    Prop *phi, *cphi;
    ArtNode* before;
    virtual void member(){ }
    virtual ~ArtNode(){ }
    virtual bool operator==(ArtNode &other)=0;
    //Level for printing
    int Level;
    int num;
};
struct UniArtNode: ArtNode{
    ArtNode *next1;
    bool operator==(ArtNode &other);
};
struct BinArtNode: ArtNode{
    ArtNode *next1, *next2;
    bool operator==(ArtNode &other);
};
struct TermArtNode: ArtNode{
    bool operator==(ArtNode &other);
};
struct BadArtNode: ArtNode{
    bool operator==(ArtNode &other);
};

//struct PostType{
//    int Flag;    // 1:UniProp, 2:BinProp
//    vector<int> B1;
//    vector<int> B2;
//};

class ART{
    private:
        vector<ArtNode*> todo;                     //紀錄遇到bad node剩下還沒做的點
        map<Node*, vector<Prop*> > CoverMap;	   //紀錄在建置時會出現Cover的情況
        //map<Expr*, int> UseTimes;                  //在建立PF的過程中需要被帶換掉的變數
        map<string, int> UseTimesString;           //在建立PF的過程中需要被帶換掉的變數，這邊換成stringi //SSACounter
        ArtNode *initNode;
        //save Max Level for Graphviz
        int MaxLevel;
        int TotalNum;
//        map<Expr*, int> M; //save the predicate
        void RecursiveBuildArt(Node*, set<int>*);
        ArtNode* BuildART(ArtNode*);
        string Prop2SSAStr(Prop*);	//convert a prop to a string in SSA form //Prop2SSAStr
        string Expr2SSAStr(Expr*);     //convert an experission to a string in SSA form //Expr2SSAStr
        void IncSSACounter(Expr*);           //之後會移到private //increse SSA counter //IncSSAConter//需要移除int 
        string PathFormula(ArtNode*, int);
        void PrintCoverMap();
        bool IsInTheTodo(ArtNode*);
        //map<Expr*, int>::iterator found(Expr*);
        void PrintOPTypeWithGraphviz(ofstream&, OPType);
        void PrintLogicTypeWithGraphviz(ofstream&, LogicType);
        void PrintPropTypeWithGraphviz(ofstream&, PropType);
        void PrintExprWithGraphviz(ofstream&, Expr*);
        void PrintPropWithGraphviz(ofstream&, Prop*);
        void PrintArtNodeWithGraphviz(ofstream&, ArtNode*, int, int);
        void PrintARTWithGraphviz(ofstream&, ArtNode*, int, int);
        void PrintSingleNWithGraphviz(ofstream&, ArtNode*);
        void WalkARTTreeWithLevel(ofstream&, ArtNode*, int);
        void PrintARTrankGraphviz(ofstream&);
        int CountMaxLevel(ArtNode*);
    public:
        ArtNode* GetInitNode(){ return initNode; }
        void SetInitNode(ArtNode *N){ initNode = N; }
        //int FindTimesMap(string);
        //string ReplaceTheName(string);
        //void RecursiveReplaceExpr(Expr*);
        //void RecursiveReplaceProp(Prop*);
        //int FindTimesMap(Expr*);
        //Expr* ExchangeExpr(Expr*);
        //Prop* ExchangeProp(Prop*);
        //Prop* ExchangeProp1(Prop*);
        //PostType CountPost(ArtNode*, Node*, vector<Prop*>*, vector<int>*);  //count Post
        Prop* ComputePost_Assign(Prop*, Expr*, Expr*);  //compute Post(phi, x:=e)
        Prop* ComputePre_Assign(Prop*, Expr*, Expr*, int);  //compute Pre(phi, x:=e)
        Prop* ComputePost_Pred(Prop*, Prop*);  //compute Post(phi, pred)
        Prop* ComputePre_Pred(Prop*, Prop*, int);  //compute Pre(phi, pred)
	Prop* Gv(Prop*, vector<Prop*>*);	
        bool IsCover(ArtNode*, Prop*);         //之後要移到private //移除Prop*//知道為什麼不拿掉Prop因為那是phi不是CFA上面的資訊
        bool IsEverCFANode(ArtNode*);          //刪除    之後要移到private //是啥??檢查一個ArtNode的對應cfa node是否存在CoverMap裡頭
        //int FindXTimes(Expr*);                 //之後要移到private //use map.find
        //void ADDphi2map(Node*, Prop*);        //之後要移到private //use map.find(ArtNode)->second.pushback()
        //void ADDpair2map(Node*, Prop*);     //之後要移到private //same
        void DELETEphiFROMmap(ArtNode*, Prop*); // the same  //formal arg. ArtNode-> Node
        //void DELETEpairFROMmap(ArtNode*, Prop*); // the same
        void DeleteArtNode(ArtNode*);
	
        void PrintTotalTree(ArtNode*);
 //       string CreatePredicate(ArtNode*, Node*, vector<Prop*>*, vector<int>*);
 //       string RecursiveProp(Prop*);
 //       string RecursiveExpr(Expr*);
 //       string RecursiveBuildPF(ArtNode*, Node*, vector<Prop*>*, vector<int>*);             //build pf
        void CFA2ART(CFA*);             //build cfa
        //為了csisat
        ArtNode* ValidateCounterExample(ArtNode *);
        void Output2File4Csisat(Prop *, Prop *);
};

//bool CompareProp(Prop *p1, Prop *p2);//用operation overloading 取代
bool CompareExpr(Expr *e1, Expr *e2); // isSubExpr(Expr* e1, Expr* e2)
#endif
